COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	CS 258		MATHEMATICAL THEORY OF COMPUTATION		JANUARY 1975
C00008 ENDMK
C⊗;
CS 258		MATHEMATICAL THEORY OF COMPUTATION		JANUARY 1975

TWO EASY PROOFS IN FOL


Here are the commands for two easy FOL proofs  based on the axioms in
the  file  INTEGE.AX[258,JMC].   After the  commands  come the  proofs
themselves followed by a reprint of the axioms. 

First comes a proof that ∀M N. SUCC  M = SUCC N ⊃ M = N.   It doesn't
use the  induction schema.  We  can write SUCC M  instead of SUCC(M),
because  we have  declared SUCC and  friends to  be prefix operators.
There is no reason not to do this for all  functions of one argument,
and maybe someday it will be automatic. 

ASSUME SUCC M = SUCC N;
∀E PEANO 2 M;
∀E PEANO2 M;
SUBSTR 1 IN 2;
∀E PEANO2 N;
TAUTEQ M=N 3 4;
⊃I 1 5;
∀I 6 M N;

Next we prove that ∀N.0+N=N.

∧I INDUCTION[P←λN.0+N=N];
∀E PLUS1 0;
ASSUME 0+N=N;
∀E PLUS2 0 N;
SUBSTR 10 IN 11;
⊃I 10 12;
∀I 13 N;
TAUT ∀N.(0+N=N) 8 9 14;


Here are the  proofs themselves run together.   The first is  steps 1
thru 7.  One gets the proof into a file FOO by the command SHOW PROOF
→ FOO;.  The manual leaves out the →.  A later version  of the system
will  record a  proof as  the interleaving  of the  commands and  the
resulting  sentences.   For the present  you will  have to interleave
them yourself. 


1  SUCCM=SUCCN  (1)  ASSUME 

2  PREDSUCCM=M    ∀E PEANO2 M 

3  PREDSUCCN=M  (1)  SUBSTR 1 IN 2 

4  PREDSUCCN=N    ∀E PEANO2 N 

5  M=N  (1)  TAUTEQ 

6  SUCCM=SUCCN⊃M=N    ⊃I 1 5 

7  ∀M N.(SUCCM=SUCCN⊃M=N)    ∀I 6 M ← M N ← N 

8  ((0+0)=0∧∀N.((0+N)=N⊃(0+SUCCN)=SUCCN))⊃∀N.(0+N)=N    ∧I (INDUCTION) 

9  (0+0)=0    ∀E PLUS1 0 

10  (0+N)=N  (10)  ASSUME 

11  (0+SUCCN)=SUCC(0+N)    ∀E PLUS2 0 , N 

12  (0+SUCCN)=SUCCN  (10)  SUBSTR 10 IN 11 

13  (0+N)=N⊃(0+SUCCN)=SUCCN    ⊃I 10 12 

14  ∀N.((0+N)=N⊃(0+SUCCN)=SUCCN)    ∀I 13 N ← N 

15  ∀N.(0+N)=N    TAUT 


Here is a reprint of the file of axioms.

COMMENT$ Here is a  set of first order axioms for  the integers based
on the successor operation written SUCC and the predecessor operation
written  PRED.   While  the  axioms  don't  mention  sets,  they  are
compatible with a  later imbedding into set theory,  because the SORT
mechanism  of FOL  relativizes the  axioms to  the domain  NATNUM, so
other domains  are possible.   It is  a blemish  that the axioms  for
PLUS, TIMES, etc.  are given as axioms, because  they are really just
definitions.  Taking these definitions  as axioms means that when  we
make the  definitions, we  are asserting  that no contradictions  are
thereby introduced.  A proper definition mechanism is conservative in
that no new  facts are introduced by  definitions.  These  particular
definitions introduce  no new  facts, but  this is  not syntactically
obvious.$


DECLARE INDVAR M M1 M2 M3 N N1 N2 N3 K K1 K2 K3 L L1 L2 L3 ε NATNUM;
DECLARE OPCONST SUCC: NATNUM → NATNUM [PRE];
DECLARE OPCONST PRED: NATNUM → INTEGER [PRE];
DECLARE INDVAR X Y Z;
DECLARE PREDPAR P(NATNUM);


AXIOM PRED:	∀N.(¬N=0 ⊃ NATNUM(PRED N));;

AXIOM PEANO:	∀N.(¬SUCC N = 0),
		∀N.PRED SUCC N = N,
		∀N.(¬N=0 ⊃ SUCC PRED N = N);;

AXIOM INDUCTION:P(0) ∧ ∀N.(P(N) ⊃ P(SUCC N)) ⊃ ∀N.P(N);;


COMMENT$ The rest of these axioms are really just definitions.$

DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM[R←475,L←470];
DECLARE PREDCONST ≥(NATNUM,NATNUM)[INF];
DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM[R←555,L←550];
DECLARE OPCONST -(NATNUM,NATNUM)=INTEGER[R←455,L←450];

AXIOM PLUS:	∀M.(M+0=M),
		∀M N.(M+SUCC N =SUCC(M+N));;

AXIOM TIMES:	∀M. M*0=0,
		∀M.M*1=1,
		∀M N. M*SUCC N = M*N+M;;

AXIOM MINUS:	∀M N. (M ≥ N ⊃ NATNUM(M-N)),
		∀M. M-0 = M,
		∀M N. (M≥N ⊃ SUCC M - SUCC N = M-N);;

AXIOM GREATER:	∀M. M≥0,
		∀M. 0≥M ⊃ M=0,
		∀M N. (M≥N ≡ SUCC M ≥ SUCC N);;